a, b:. (a = b)  (a =b b) 

latex

Definitions	x. t(x), x:A  B(x), , b, p =b q, x:AB(x), Type, t  T, x.A(x), x:A. B(x), P  Q, P & Q, P  Q, P  Q, s = t,
Lemmas	iff wf, eq bool wf, assert wf, bool wf, assert of eq bool, iff functionality wrt iff, all functionality wrt iff